| Definitions |  x:A. B(x), P   Q,  , t  T,   x. t(x), A c B, P & Q, S  T, tagged-messages(l;s;v;L), State(ds), D realizes2 es.P(es), vartype(i;x), E, loc(e), valtype(e), kind(e), isrcv(e), lnk(e), sends(l;e), x when e, val(e), ES(the_w), es-T(es), t.1, t.2, es_info(es), rcvtype(e), acttype(e), es-eq(es), es-pred?(es), es_val(es), es-oaxioms(es), es_state_when(es;e), es-M(es), tag(e), es-V(es), act(e), es_init(es), es-Trans(es), es_time(es), {T}, f(x)?z, x dom(f), f(x),  A,  T, True, False, if b then t else f fi , islocal(k), act(k), ff, valtype(i;a), loc(e), isrcv(k), lnk(k), tag(k), time(e), kind(e), kindcase(k; a.f(a); l,t.g(l;t) ),  b, isl(x), outr(x), outl(x), tt, SQType(T), rcv(l,tg),  b, Top, MsgA, Valtype(da;k), M.da(a), Msg, P  Q, P Q, P  Q, mlnk(m), x(s), es is an event system of D,  x:A. B(x), (Msg on l), haslink(l;m), @i: with declarations ds:dsda:da k(v) sends f s v on link l, PossibleWorld(D;w), M.ds(x), M(i), M.init(x,v), M.pre(a,s), M.ef(k,x,s,v,w), M.send(k;l;s;v;ms;i), M.frame(k affects x), M.sframe(k sends <l,tg>), M.aframe(k affects x), M.bframe(k sends on l), with declarations ds:dsda:dak(v) sends f s v on link l, z != f(x) P(a;z), mk-ma, x : v, deq-member(eq;x;L), reduce(f;k;as), Y, Knd,  , Unit, Msg(M), a declared in M, unsolvable M.pre(a,s), Msg, msg(l;t;v), state_when(e), state_when(e), vartype(i;x), act(e), locl(a),  , a = b, w_sends(e;l), tagged-list-messages(s;v;L) |
| Lemmas | d-realizes2-implies-realizes, d-single-sends wf, Id wf, lsrc wf, ma-state wf, ma-valtype wf, fpf-cap wf, Knd wf, Kind-deq wf, rcv wf, fpf wf, IdLnk wf, es-vartype wf, id-deq wf, top wf, es-E wf, es-loc wf, es-valtype wf, es-kind wf, assert wf, es-isrcv wf, es-lnk wf, es-Msg wf, mlnk wf2, Msg wf, es-sends wf, es-Msgl wf, map wf, tagged-list-messages wf, msg wf, fpf-cap-void-subtype, es-when wf, es-val wf, possible-world wf, fair-fifo wf, world wf, eqof eq btrue, loc wf, w-E wf, w-info wf, w-loc-lemma, w-act wf, w-action wf, not wf, w-isnull wf, subtype rel wf, squash wf, true wf, w-kind-lemma, w-kind wf, w-M wf, Id sq, w-TA wf, w-ekind wf, tagof wf, IdLnk sq, ma-da wf, ifthenelse wf, fpf-empty wf, rationals wf, locl wf, pi1 wf, pi2 wf, fpf-single wf, false wf, lnk wf, isrcv wf, eq id wf, bool wf, iff transitivity, eqtt to assert, assert-eq-id, bnot wf, eqff to assert, assert of bnot, not functionality wrt iff, mlnk wf, bool cases, eqof wf, bool sq, deq property, kind wf, w-a-not-null, w-time wf, assert of bor, product-deq wf, idlnk-deq wf, w-a wf, bfalse wf, or functionality wrt iff, subtype rel transitivity, w-Msg wf, list-set-type2, assert-eq-lnk, w sends-wf2 |
Type, da:a:Knd fp
f:((tg:Id 
(State(ds)